\documentclass[orivec,envcountsame]{llncs}
\usepackage{verbatim}
%\usepackage[T1]{fontenc}
\usepackage[latin1]{inputenc}
\usepackage{amsfonts, amssymb, amsmath}

\input{macros}
\input{proofmacros}
\pagestyle{plain}

\title{Timed Mobile Systems}

\author{Andrew Hughes\thanks{Corresponding author.} \and Mike Stannett}

\institute{Department of Computer Science, University of Sheffield, \\
  Regent Court, 211 Portobello Street, Sheffield S1 4DP, UK. \\
  \email{\{a.hughes,~m.stannett\}@dcs.shef.ac.uk}
}

\begin{document}

\maketitle

\begin{abstract}

We present \emph{TNT}, a novel calculus combining explicit clocks and
run-to-completion semantics with mobility, and demonstrate its
suitability for modelling complex hierarchical systems with dynamic
topology.

\end{abstract}

\section{Introduction}
\label{introduction}

A standard feature of concurrent systems modelling is the use of
\emph{synchronisation} to model \emph{interaction}. Indeed, this is the
defining concept of CCS \cite{milner:ccs}. Calculi that include
\emph{localities} -- for example the \emph{ambient calculus} \cite{amb}
-- also allow the notion of componentisation to be explicitly realised
by forming processes into a hierarchy. The inclusion of locality
naturally leads to \emph{mobility}, the ability of a system to change
its topological structure unilaterally. Consequently, the ambient
calculus and its analogues are well positioned to model distributed
systems in which resources can migrate from one location to another.

What tends to be absent from these models, however, is the notion of
behaviour also being governed by time, or at least, some notion of
workflow. Some calculi maintain continuous time values
\cite{tccs,beaten:timing,brics:lee}, but the notion that work typically
occurs in stages is modelled only abstractly. For example, consider an
environment inhabited by the members of a factory team. The team
receives a series of tasks to execute, which require the team members to
communicate with one another. At some point, the first task is completed
and the team moves on to the next. Modelling this in a setting where the
number of workers cannot be predicted typically requires the use, either
of \emph{global} synchronisation, or else (which we reject) of an
infinite set of defining equations.

The idea of global synchronisation via \emph{clock signals} is made explicit by
various process algebras, including TPL \cite{hennessy:tpl}, PMC
\cite{pmc}, CSA \cite{csa} and CaSE \cite{case,norton05alg}. Our contribution is
to combine the notions of \emph{location}, \emph{clocks} and \emph{mobility} to
create a calculus capable of modelling dynamic componentised systems, where
behaviour is defined both by interactions between individual processes and by
responses to external stimuli, as represented by clock signals. A number of
calculi \cite{lee:realtime,satoh:phd,webpi} have already attempted to combine
mobility with continuous time values, but we believe the aggregation
of mobility and discrete clocks to be novel.

Our calculus, \emph{Typed Nomadic Time} (TNT) provides a framework for
modelling such systems, with practical applicability very much in
mind. The object of this paper is to demonstrate its underlying formal
theory, derived in part from existing research in the area, via a
description of its syntax, operational semantics and type system. Our
long term aim is to leverage TNT as a foundation for creating concurrent
systems within a programmatic context. This will allow the specification
of system interactions to be shifted directly from the theoretical
domain into an implementation backed by a formal methodology, helping in
turn to improve industrial adoption of concurrent techniques.

\section{Typed Nomadic Time}
\label{tnt}

In this section, we present the syntax, operational semantics and type
system of TNT. In creating this calculus, our aim is not to create ``yet
another process calculus,'' but rather a framework which allows
industrially relevant systems to be modelled in the simplest and most
elegant way possible. We have re-used well-established concepts where
appropriate.

\subsection{Syntax}

The formal syntax of TNT is shown in (\ref{eqn:tnt-syntax}), where
$\expr$ and $\exprb$ define possible process terms and $\ambop$ the
available mobility primitives. We assume a countable set of actions,
$\actions = \names \cup \conames \cup \{\tau\}$, ranged over by $\alpha$
and $\beta$, where the elements of $\names$ are drawn from an infinite
set of \emph{names}, and $\conames$ is the corresponding set of
\emph{co-names}, $\{\overline{a} \mid a \in \names\}$. $\timers$ is a
countably infinite set of \emph{clocks} over which $\sigma$ ranges,
while $m$ represents an arbitrary \emph{environ name}. In particular,
$m$ may be equal to the empty string, $\epsilon$, thus facilitating the
use of anonymous environs\footnote{A primary motivation for this is that
it allows TNT to be a conservative extension of CaSE. To obtain an
encoding for clock hiding, there must be a way of mapping the operator
to an equivalent environ.}. $X$ ranges over a countably infinite set of
variables, which are used to bind process behaviour in recursive process
definitions.  As usual, we often write $a$ for $\{a\}$, so for example
$P \res{a}$ means $P \res{\{a\}}$.

\begin{equation}
  \begin{aligned}
    \expr, \exprb \quad \mathrel{::=} \quad &
      \nil  \mid
      \Omega \mid
      \Delta \mid
      \Delta_{\sigma} \mid
      \alpha . \expr  \mid
      \expr + \exprb \mid
      \expr \mathrel{\!|\!} \exprb \mid
      \timeout{\expr}{\sigma}{\exprb} \mid \\
    & \stimeout{\expr}{\sigma}{\exprb} \mid 
      \mu X . \expr \mid
      X \mid 
      \expr \res{A} \mid
      \locv{m}{\expr}{\exprb}{\vec{\sigma}} \mid
      \ambop . \expr \\
   \ambop \quad \mathrel{::=} \quad & \tntin{m} \mid \tntout{m} \mid \tntopen{m} \mid
      \procin{\beta}{m} \mid \procout{\beta}{m} \mid \bin \mid
      \bout \mid \bopen
   \end{aligned}
   \label{eqn:tnt-syntax}
\end{equation}


At its heart, TNT is a conservative extension of Milner's CCS.
Specifically, within each environment lie processes which interact with
one another via \emph{handshake} synchronisation; to proceed, one
process must emit an action as another simultaneously emits the
corresponding co-action.  This is something TNT shares with its
predecessor, CaSE, from which it also acquires the following features:

\begin{enumerate}
\item Multiple \emph{abstract clocks}, denoted $\sigma, \rho, \dots$,
      which are interpreted not as quantitative values, but in a
      qualitative fashion as signals of recurring events.
\item Two \emph{timeout} operators, \emph{fragile} ($\timeout{E}{\sigma}{F}$) and
      \emph{stable} ($\stimeout{E}{\sigma}{F}$), which allow the behaviour of
      processes to depend upon the occurrence of specific clock
      signals.
\item Two \emph{timelock} operators, $\Delta$ and $\Delta_{\sigma}$,
      which prevent all clocks, or a single
      clock $\sigma$, from ticking, respectively.
\item The concept of \emph{maximal progress} or
      prioritisation.  A signal from a clock may be pre-empted by a process that engages in a higher priority
      transition.  In CaSE, the only such transition is the internal action,
      $\tau$, which results in processes performing maximal
      behaviour before allowing a clock to tick.
\item Encapsulation, realised in CaSE by the process of \emph{clock
      hiding}, which is analogous to the notion of hiding found in
      CSP \cite{hoare:csp78}.  This facilities the amalgamation of clock ticks
      from a child component into the cycle of its parent.
\end{enumerate}

Clocks and their associated operators are retained verbatim within
TNT, while \emph{encapsulation} and \emph{prioritisation}, which permit
\emph{componentisation} and \emph{synchronous event cycles}
respectively, are extended.

Within CaSE, encapsulation is implicitly realised by the notion of clock
hiding.  When a clock, $\sigma$, is hidden it appears indistinguishable
from an internal action to observers outside the scope of the hiding
operator.  When combined with maximal progress, an entire subsystem
(defined by the clock's scope) appears equivalent to a single process,
with respect to the cycles of clocks with a wider scope.  Just as with
processes, the subsystem performs maximal behaviour before
any of the parent's clocks tick.

In TNT, we make this notion explicit by representing the boundaries of
the component syntactically.  These scope boundaries indirectly affect
processes, with interaction being disallowed between those in separate
environments.  This construction looks to the existing area of
\emph{localities} \cite{obslocal,pawl}, which have been used in various
ways in a number of existing calculi.  We draw our inspiration mostly
from Cardelli and Gordon's ambient calculus, which forms the framework
for many of the results in this field.

Our localities or \emph{environs} are realised in the process form
$\locv{m}{\expr}{\exprb}{\vec{\sigma}}$.  The environ has a name
($m$), some behaviour ($\expr$), a security model in the form of a
`bouncer' ($\exprb$) and a set of clocks, $\vec{\sigma}$.  Environs implement clock hiding;
in terms of the corresponding CaSE operator, we have $\seml E \hide{\sigma} \semr \eqdef \loc{}{E}{\Omega}{\sigma}$.

The environ, $m$, is used with TNT's mobility primitives, as in Cardelli
and Gordon's ambient calculus.  We retain their $in\ m$, $out\ m$ and $open\
m$ primitives, but represent them using the mnemonics $\tntin{m}$,
$\tntout{m}$ and $\tntopen{m}$ to prevent confusion with the names of
actions.  In addition, we add two primitives for process mobility,
$\procin{\beta}{m}$ and $\procout{\beta}{m}$, which allow objective
mobility to occur via synchronisation on the action $\beta$.

Transitions are divided into three sets:

\begin{enumerate}
\item a set of \emph{high priority transitions} (denoted $\highpris$), which includes $\tau$ and
      the mobility transitions, $\tin$, $\tout$ and $\topen$.
\item a set of \emph{low priority transitions}, which includes all
      clock transitions.
\item a set of \emph{independent transitions} with labels drawn from the
      set $\names \cup \conames$. These neither pre-empt nor inhibit any other
      transitions.
\end{enumerate}

If a process may emit a transition in $\highpris$, then low-priority
transitions are prevented from occurring.  This also applies to CaSE,
where $\highpris$ is simply $\{ \tau \}$.

Finally, TNT provides a method for security based on research into
safe ambients \cite{sangiorgi:mobsafeambients}.  \emph{Grave
interferences} occur when two logically different mobility transitions may
occur at the same time, a scenario which leads to radically
different reductions.  These are unlike normal interferences, where more
than one action competes for synchronisation, and tend to represent
errors rather than an intentional notion of competition for resources.
They occur because, unlike actions, the mobility primitives in the
ambient calculus occur in isolation rather than in pairs.  Both safe
ambients and TNT solve this problem by introducing the equivalent of
co-names for mobility primitives, so that a similar synchronisation
process must take place before movement occurs.

In TNT, this is realised by \emph{bouncers}.  Named after the staff who
restrict access to a night club\footnote{American usage:
doorman/woman.}, the bouncer is an additional property of an environ
which appears in the top right of the expression.  It has no real
behaviour of its own, but instead performs the job of protecting the
environ, being a process with a limited choice of available
constructs\footnote{This limited choice is only explicitly imposed by
the type system.  There is no restriction in the abstract syntax.}.  The
bouncer provides a structured selection of co-primitives ($\bin$,
$\bout$ and $\bopen$), and dictates which mobility transitions may
occur, and when.

This implementation differs from that in other calculi, such as
Sangiorgi's safe ambients, both by specialising the process which may provide
these co-primitives and also by attaching it to the environ itself.
When a TNT environ moves, its bouncer moves with it and so an
association is maintained between the two which is not present where the
co-primitives are provided by an normal arbitrary process.  To maintain
this distinction between bouncers and normal processes, $\Omega$ is used
to represent a bouncer with no behaviour, as opposed to CCS's $\nil$.  The
effect of adding this process term is considered in more detail in section
\ref{typesys}, where we discuss the type system.

\subsection{Operational Semantics}

This section gives TNT an operational semantics in terms of a labelled
transition system, $(\procs, \labels, \rightarrow)$, defined
up to structural congruence.  $\procs$ is the set of TNT expressions; $\labels$ the
alphabet comprising actions, clocks and mobility primitives; and $\rightarrow$ the
transition relation.  Transitions with labels in
$\actions$ are known as \emph{action transitions}, those in $\timers$ as
\emph{clock transitions} and those in $\mobprim$ as \emph{mobility
transitions}.  The transition relation, $\mathop{\rightarrow} \mathrel{\subseteq}
\procs \times \labels \times \procs$ is defined in Table \ref{tab:casesubset}.
We use $E$, $F$ and $G$ to range over process terms; $\sigma$ and $\rho$ over the
set of clocks ($\timers$); $\alpha$ over the set of actions
($\actions$); $h$ over $\highpris$; $a$ and $b$ over 
$\symbols \eqdef
\left(\labels \setminus \{\tau\}\right) 
\cup 
\{ \tntin{m}, \tntout{m}, \tntopen{m} \} 
\cup
\{ \procin{\beta}{m}, \procout{\beta}{m} \}
$;
$\kappa$ over $\actions \cup \mobprim$;
and $\gamma$ over $\actions \cup \timers \cup \mobprim$.

\clearpage
\begin{proposition}
The semantics exhibit the following properties:
\begin{enumerate}
\item prioritisation;
$E \derives{\sigma}$ implies $E \nderives{h}$ 
\item time determinacy; $E \derives{\sigma} E'$ and $E
\derives{\sigma} E''$ implies $E' = E''$.\qed
\end{enumerate}
\end{proposition}

Structural congruence is the least congruence relation that satisfies
the laws given in Table \ref{tab:structcong}, allowing structural
rearrangement and simplification of process terms. $A$, $B$ and $C$
range over subsets of \symbols.  Notably, the rules allow multiple
restriction operators to be combined into a single set (StrResRes).

\begin{table}
 \caption{Structural Congruence Laws}
 \label{tab:structcong}
 \vspace{-3mm}
  \shrule \centering
  \begin{tabular}{rcrcl}
  StrSum1 & \quad\quad &  
  $E + F$              & $\equiv$ & $F + E$
\\
  StrSum2 &&  
  $E + (F + G)$        & $\equiv$ & $(E + F) + G$
\\
  StrPar1 &&  
  $E \pc F$            & $\equiv$ & $F \pc E$
\\
  StrPar2 &&  
  $E \pc (F \pc G)$    & $\equiv$ & $(E \pc F) \pc G$
\\
  StrIdent &&  
  $E \pc \nil$         & $\equiv$ & $E$
\\
  StrResRem &&  
  $\nil \res{A}$       & $\equiv$ & $\nil$
\\
  StrResRes &&  
  $E \res{A} \res{B}$  & $\equiv$ & $E \res{A \cup B}$
  \end{tabular}
  \shrule
\end{table}

Table \ref{tab:casesubset} shows the operational semantics, some of
which is inherited from CaSE, for which the reader is referred to
\cite{case}.  However, commutativity is now implied by the presence of
structural congruence, and the use of the restriction $E \mid F
\nderives{h}$ enforces prioritisation.  Rule $LHd1$ provides the
conversion of ticks emitted by the hidden clocks to silent actions: if
$E$ can perform a $\sigma$ transition, then it performs a $\tau$
transition in any context where $\sigma$ is hidden.  Also included in
the table is the rule $SCong$, which links the structural congruence
rules to the labelled transition system, and rules which allow the
mobility prefix, $\ambop$, to evolve, thus completing the semantics for
expressions.

\begin{table}
  \caption{Semantics}
 \label{tab:casesubset}
 \vspace{-3mm}
  \shrule
 \begin{center}
 \begin{tabular}{rlrl}
     \Rule{Idle}
     {-}
     {\nil \lderives{\sigma} \nil}
     {}
     &
     \quad \Rule{Act}
     {-}
     {\alpha . E \derives{\alpha} E}
     {}
     \\[3ex]
     \Rule{Patient}
     {-}
     {a.E \derives{\sigma} a.E}
     {}
     &
     \Rule{Stall}
     {-}
     {\Delta_{\sigma} \derives{\rho} \Delta_{\sigma}}
     {\rho \ne \sigma}
     \\[3ex]
     \Rule{Sum1}
     {E \derives{\kappa} E^\prime}
     {E + F \derives{\kappa} E^\prime}
     {}
     &
     \Rule{Par1}
     {E \derives{\kappa} E^\prime}
     {E \;|\; F \derives{\kappa} E^\prime \;|\; F}
     {}
     \\[3ex]
     \Rule{Sum2}
     {E \derives{\sigma} E^\prime, F \derives{\sigma} F^\prime}
     {E + F \derives{\sigma} E^\prime + F^\prime}
     {}
     &
      \Rule{Par2}
      {E \derives{a} E^\prime,
        F \derives{\overline{a}} F^\prime}
      {E \;|\; F \derives{\tau} E^\prime \;|\; F^\prime}
      {}
     \\[3ex]
      \Rule{Par3}
      {E \derives{\sigma} E^\prime,
        F \derives{\sigma} F^\prime,
        E \;|\; F \nderives{h}}
      {E \;|\; F \derives{\sigma} E^\prime \;|\; F^\prime}
      {}
     &
      \Rule{FTO1}
      {E \nderives{h}}
      {\timeout{E}{\sigma}{F} \derives{\sigma} F}
      {}
     \\[3ex]
      \Rule{FTO2}
      {E \derives{\gamma} E'}
      {\timeout{E}{\sigma}{F} \derives{\gamma} E'}
      {\gamma \ne \sigma}
     &
      \Rule{STO1}
      {E \nderives{h}}
      {\stimeout{E}{\sigma}{F} \derives{\sigma} F}
      {}
     \\[3ex]
      \Rule{STO2}
      {E \derives{\kappa} E'}
      {\stimeout{E}{\sigma}{F} \derives{\kappa} E'}
      {}
     &
      \Rule{STO3}
      {E \derives{\rho} E'}
      {\stimeout{E}{\sigma}{F} \derives{\rho} \stimeout{E'}{\sigma}{F}}
      {\rho \ne \sigma}
     \\[3ex]
      \Rule{Rec}
      {E \derives{\gamma} E'}
      {\mu X.E \derives{\gamma} E' \{ \mu X.E / X\}}
      {}
      &
      \Rule{Res}
      {E \derives{\gamma} E'}
      {E \res{a} \derives{\gamma} E' \res{a}}
      {\gamma \ne a}
     \\
      \Rule{LHd1}
      {E \derives{\sigma} E'}
      {\locv{m}{E}{B}{\vec{\sigma}} \derives{\tau} \locv{m}{E'}{B}{\vec{\sigma}}}
      {\sigma \in \vec{\sigma}}
  &
        \Rule{LHd2}
      {E \derives{h} E'}
      {\locv{m}{E}{B}{\vec{\sigma}} \derives{h} \locv{m}{E'}{B}{\vec{\sigma}}}
      {}
  \\[3ex]
      \Rule{LHd3}
      {E \derives{\rho} E',
       E \nderives{\sigma}}
      {\locv{m}{E}{B}{\vec{\sigma}} \derives{\rho} \locv{m}{E'}{B}{\vec{\sigma}}}
      {\rho \not \in \vec{\sigma}, \sigma \in \vec{\sigma}}
&
      \Rule{Cap1}
      {-}
      {\ambop . E \derives{\ambop} E}
      {}
  \\[3ex]
  \Rule{Cap2}
  {-}
  {\ambop . E \derives{\sigma} \ambop . E}
  {}
&
     \quad \Rule{SCong}
     {E \equiv E', E' \derives{\gamma} F', F' \equiv F}
     {E \derives{\gamma} F}
     {}
  \\
  \\
  \multicolumn{4}{c}{
  \Rulea{InEnv}
  {E \derives{\tntin{m}} E', B_1 \derives{\bin} B'_1}
  {\locv{n}{E}{B_2}{\vec{\sigma}} \;|\;
  \locv{m}{G}{B_1}{\vec{\rho}}
  \derives{\tin}
  \locv{m}{G \pc \locv{n}{E'}{B_2}{\vec{\sigma}}}{B'_1}{\vec{\rho}}}
  {}
  }
  \\[3ex]
  \multicolumn{4}{c}{
  \Rulea{OutEnv}
  {E \derives{\tntout{m}} E', B_1 \derives{\bout} B'_1}
  {\locv{m}{G \pc \locv{n}{E}{B_2}{\vec{\sigma}}}{B_1}{\vec{\rho}}
  \derives{\tout}
  \locv{n}{E'}{B_2}{\vec{\sigma}} \pc
  \locv{m}{G}{B'_1}{\vec{\rho}}}
  }
  {}
  \\[3ex]
  \multicolumn{4}{c}{
  \Rulea{Open}
  {E \derives{\tntopen{m}} E', B_1 \derives{\bopen} B'_1}
  {\locv{n}{E \;|\; \locv{m}{F}{B_1}{\vec{\sigma}}}{B_2}{\vec{\gamma}}
  \derives{\topen} 
  \locv{n}{E' \;|\; F}{B_2}{\vec{\gamma} \cup \vec{\sigma}}}
  {}
  }
  \\[3ex]
  \multicolumn{4}{c}{
  \Rulea{ProcIn}
  {E \derives{a} E',
  F \xderives{\procin{a}{m}} F',
  B_1 \derives{\bin} B'_1}
  {((E \pc G) \res{A}) \pc F \pc 
  \locv{m}{H}{B_1}{\vec{\sigma}}
  \derives{\tin}
  {(G \res{A}) \pc F' \pc \locv{m}{H \pc E'}{B'_1}{\vec{\rho}}}
  }
  }
  {}
  \\[3ex]
  \multicolumn{4}{c}{
      \Rulea{ProcOut}
  {E \derives{a} E',
  F \xderives{\procout{a}{m}} F',
  B_1 \derives{\bout} B'_1}
  {\locv{m}{((E \;|\; G) \res{A}) \pc F}{B_1}{\vec{\sigma}}
  \derives{\tout}
  {E' \pc \locv{m}{(G \res{A}) \pc F'}{B'_1}{\vec{\sigma}}}
  }
  }
  {}
 \end{tabular}
  \end{center}
  \shrule
\end{table}

The remaining semantics focus on mobility.  $InEnv$ allows a $\tin$
transition to occur and $n$ to move into $m$ if matching $\tntin{m}$ and
$\bin$ transitions are available from the process $\tntin{m}.E$ and
bouncer, $B_1$.  Conversely, $OutEnv$ concerns the interaction between
$\tntout{m}.E$ and $\bout$, allowing a $\tout$ transition to occur and
$n$ to move outside $m$.  Likewise, $\tntopen{m}$ causes a $\topen$
transition to occur when both an $\tntopen{m}$ and an $\bopen$
transition are available.  The named environ, $m$, is destroyed and the
two clock contexts unified.

Finally, $ProcIn$ and $ProcOut$ describe the movement of processes
between environs.  In both rules, $E$ moves due to a mobility primitive
which is part of $F$.  This occurs if an $a$ transition takes place in
the presence of matching $\procin{a}{m}$ and $\bin$, or
$\procout{a}{m}$ and $\bout$, actions.  An appropriate mobility transition ($\tin$ or $\tout$) is
emitted as a result of this three-way synchronisation.  Process
mobility, in this form, is \emph{objective}.  The process which emits
the mobility primitive synchronises with a partner process, and it is
this partner which actually moves.  The partner is necessarily a process in
the same environ, due to the scoping of actions described above.

Such behaviour is initially difficult to understand, but can be made
clearer with a simple example.  Consider the composition
%
\[
  \procin{go}{m}.E \pc go.F \pc \loc{m}{\nil}{\bin.\bout.\Omega}{\sigma}
\]
%
where the first process may perform $\procin{go}{m}$, causing
the second to move,
%
\begin{equation}
\procin{go}{m}.E \pc go.F \pc \loc{m}{\nil}{\bin.\bout.\Omega}{\sigma} ~\derives{\tin}~
E \pc \loc{m}{F \pc \nil}{\Omega}{\sigma}
\label{eqn:binbout}
\end{equation}
%
with the continuation, $F$, continuing to evolve in the
environ $m$.  Process mobility in this objective form can nonetheless be used
to perform \emph{subjective} movement.  Since processes can fork, a process that
wishes to move can evolve into a situation where it is composed with a new process that exhibits the required movement
primitive. For example, suppose the continuation $F$ is defined as
%
\[
F \eqdef leave.F^\prime \pc \procout{leave}{m}
\]
%
where the process on the right moves the one on the left
outside $m$. Then the derivation (\ref{eqn:binbout}) continues with the transition
%
\[
E \pc \loc{m}{leave.F^\prime \pc \procout{leave}{m}.\nil \pc
 \nil}{\bout.\Omega}{\sigma} 
~\derives{\tout}~
E \pc F^\prime \pc \loc{m}{\nil \pc \nil}{\Omega}{\sigma}
\]
%
to give a final process which is very similar to the original.
More generally, subjective movement may be encoded (subject to
appropriate bouncers being defined) as
%
\begin{eqnarray*}
\seml \sprocin{m}{E}.F \semr & \eqdef & z.E \pc \procin{z}{m}.F \\
\seml \sprocout{m}{E}.F \semr & \eqdef & z.E \pc \procout{z}{m}.F
\end{eqnarray*}
%
where $E$ is the process that will move into $m$, $F$ is the
continuation and $z$ is a new name. 

Notice that channels may become unrestricted due to the movement of an
expression into a different environ.  For example, $((E \pc G) \res{A})$
becomes $G \res{A}$ when $E$ changes position.  As a result, any names
that were restricted by $A$ in $E$ are no longer
restricted following its movement.

\subsection{Type System}
\label{typesys}

We now consider the specification of a simple type system for the
calculus, which fulfils two main goals:

\begin{enumerate}
\item It ensures the sanity of a given TNT construction, which is
  implicit in the examples above.  This is primarily achieved by
  ensuring that normal process primitives and the primitives used by
  bouncers remain distinct.  For example,
  $\tntin{n}.\bin.\nil$ should not be a valid bouncer,
  especially as $\tntin{n}$ suggests that the bouncer (and its environ)
  should move inside $n$.
\item It extends and refines our control over mobility by adding a
      secondary mechanism orthogonal to the use of bouncers.
\end{enumerate}

Our rudimentary type system is inspired in part by that of the ambient calculus,
specifically the notion of groups presented in \cite{ambienttypes} and
\cite{m3}.  Each process is assigned a group type, which determines the
use of the mobility primitives.  Each group is a tuple comprising four
sets of environ names\footnote{Each group $g$ is defined abstractly to
be of kind $Group$.}:

\begin{tabular}{rlcl}
$\quad \bullet$ & $\mathscr{R}$ & -- & Environs in which the process may
 \emph{reside} \\
$\bullet$ & $\mathscr{O}$ & -- & Environs which it may \emph{open} \\
$\bullet$ & $\mathscr{L}$ & -- & Environs which it may \emph{leave} \\
$\bullet$ & $\mathscr{E}$ & -- & Environs which it may \emph{enter}
\end{tabular}

$\mathscr{L}$ and $\mathscr{E}$ form subsets of $\mathscr{R}$, as
clearly, if a process may enter or leave a environ, it must also be able
to reside within it.  As an example, consider the group
$(\{n\},\emptyset, \emptyset,\{n\})$.  Processes of this type may enter
and reside in $n$, but, once there, they may not leave.  They also lack
the ability to destroy $n$.  We write $g(\mathscr{R})$,
$g(\mathscr{O})$, $g(\mathscr{L})$ and $g(\mathscr{E})$ for the
components of the group $g$.

The type system is presented in Table \ref{tab:basictypes}; the general
syntax for a type $T$ is given by\footnote{Notice that no construct is
available (none is needed) for recovering the components of a product
type in this system.}

\begin{equation*}\begin{aligned}
T \mathrel{::=} & \quad P \mid Act \mid Clock \mid Name \mid Bouncer \mid
 Environ \\
P \mathrel{::=} & \quad g \mid P \oplus P \mid P \otimes P \mid \pi_L P \mid
 \pi_R P \\
                & \quad \text{where $g \colon Group$ ranges over group types.}
\end{aligned}
\end{equation*}

The rule $Env$ states that if $\xi$ of type $T$ is a member of
$\Gamma$, then a typing derivation $\vdash \xi : T$ may be made in the
context of $\Gamma$.  This forms the basis of all later rules.  Notice
that our system is naturally polymorphic; both $\nil$ and $\Delta$ can
have any group type $g$.  In contrast, $\Omega$ can only be typed as a
$Bouncer$, thus distinguishing it from the behaviourally equivalent
process, $\Delta$.  Notice also that $FTO$ and $STO$ require that
$\sigma$ is typeable as a clock, another restriction which makes
explicit a number of issues implied in the syntax.  $BRec$ allows
recursive bouncers to be defined, while $BIn$, $BOut$ and $BOpen$ allow
an existing bouncer, $B$, to be prefixed with one of the three bouncer
primitives ($\bin$, $\bout$ and $\bopen$)


\begin{table}
  \caption{Types}
  \label{tab:basictypes}
 \vspace{-3mm}
  \shrule
 \begin{center}
 \begin{tabular}{rlrl}
     \Rule{Env}
     {\xi : T \in \Gamma}
     {\Gamma \vdash \xi : T}
     {}
  &
  \Rule{Nil}
     {\Gamma \vdash g : Group}
     {\Gamma \vdash \nil : g}
     {}
  \\[3ex]
     \Rule{BNil}
     {-}
     {\Gamma \vdash \Omega : Bouncer}
     {}
     &
     \Rule{Stop}
     {\Gamma \vdash g : Group}
     {\Gamma \vdash \Delta : g}
     {}
     \\[3ex]
     \Rule{Stall}
     {\Gamma \vdash \sigma : Clock, g : Group}
     {\Gamma \vdash \Delta_\sigma : g}
     {}
     &
     \Rule{Act}
     {\Gamma \vdash \alpha : Act, E : g : Group}
     {\Gamma \vdash \alpha . E : g}
     {}
  \\[3ex]
     \Rule{Rec}
     {\Gamma \vdash E : g : Group}
     {\Gamma \vdash \mu X.E : g}
     {}
     &
     \Rule{Res}
     {\Gamma \vdash a : Name, E : g : Group}
     {\Gamma \vdash E \res{a} : g}
     {}
  \\[3ex]
   \Rule{SumC}
   {\Gamma \vdash E : g : Group, F : g' : Group}
   {\Gamma \vdash E + F : g \oplus g'}
   {}
   &
   \Rule{ParC}
   {\Gamma \vdash E : g : Group, F : g' : Group}
   {\Gamma \vdash E \pc F : g \otimes g'}
   {}
   \\[3ex]
   \Rule{SumL}
   {\Gamma \vdash E + F : g : Group}
   {\Gamma \vdash E' : \pi_{L} g}
   {(E \derives{\kappa} E')}
   &
   \Rule{SumR}
   {\Gamma \vdash E + F : g : Group}
   {\Gamma \vdash F' : \pi_{R} g}
   {(F \derives{\kappa} F')}
   \\[3ex]
   \Rule{FTOC}
   {\Gamma \vdash E : g : Group, F : g' : Group}
   {\Gamma \vdash \timeout{E}{\sigma}{F} : g \oplus g'}
   {}
   &
   \Rule{STOC}
   {\Gamma \vdash E : g : Group, F : g' : Group}
   {\Gamma \vdash \stimeout{E}{\sigma}{F} : g \oplus g'}
   {}
   \\[3ex]
   \Rule{FTOL}
   {\Gamma \vdash \timeout{E}{\sigma}{F} : g : Group}
   {\Gamma \vdash E' : \pi_{L} g}
   {(E \derives{\gamma} E', \gamma \ne \sigma)}
   &
   \Rule{FTOR}
   {\Gamma \vdash \timeout{E}{\sigma}{F} : g : Group}
   {\Gamma \vdash F : \pi_{R} g}
   {}
   \\[3ex]
   \Rule{STOL}
   {\Gamma \vdash \stimeout{E}{\sigma}{F} : g : Group}
   {\Gamma \vdash E' : \pi_{L} g}
   {(E \derives{\kappa} E')}
   &
   \Rule{STOR}
   {\Gamma \vdash \stimeout{E}{\sigma}{F} : g : Group}
   {\Gamma \vdash F : \pi_{R} g}
   {}
   \\[3ex]
  \Rule{BRec}
  {\Gamma \vdash B : Bouncer}
  {\Gamma \vdash \mu X.B : Bouncer}
  {}
  &
  \Rule{BIn}
  {\Gamma \vdash B : Bouncer}
  {\Gamma \vdash \bin .B : Bouncer}
  {}
  \\[3ex]
  \Rule{BOut}
  {\Gamma \vdash B : Bouncer}
  {\Gamma \vdash \bout .B : Bouncer}
  {}
  &
  \Rule{BOpen}
  {\Gamma \vdash B : Bouncer}
  {\Gamma \vdash \bopen .B : Bouncer}
  {}
  \\[3ex]
  \multicolumn{4}{c}{
  \Rulea{STOS}
   {\Gamma \vdash \stimeout{E}{\sigma}{F} : g : Group}
   {\Gamma \vdash \stimeout{E'}{\sigma}{F} : g}
   {(E \derives{\rho} E', \rho \ne \sigma)}
  }
  \\[3ex]
  \multicolumn{4}{c}{
   \Rulea{BSum}
   {\Gamma \cup \Gamma^\prime \vdash B : Bouncer,
   \Gamma \cup \Gamma^\prime  \vdash B^\prime : Bouncer}
   {\Gamma \cup \Gamma^\prime \vdash B + B^\prime : Bouncer}
   {}
  }
  \\[3ex]
  \multicolumn{4}{c}{
     \Rulea{Environ}
     {\Gamma \vdash m : Environ,
     \Gamma \vdash E : g : Group,
     \Gamma \vdash B : Bouncer,
     m \in g(\mathscr{R})}
     {\Gamma \vdash \loc{m}{E}{B}{\vec{\sigma}} : g}
     {}
  }
  \\[3ex]
  \multicolumn{4}{c}{
     \Rulea{EnvIn}
     {\Gamma \vdash m : Environ,
  \Gamma \vdash E : g : Group,
  m \in g(\mathscr{E})}
     {\Gamma \vdash \tntin{m}.E : g}
     {}
  }
     \\[3ex]
  \multicolumn{4}{c}{
     \Rulea{EnvOut}
     {\Gamma \vdash \loc{n}{\loc{m}{E}{B_1}{\vec{\sigma}}}{B_2}{\vec{\rho}} : g : Group,
  m \in g(\mathscr{L}),
  n \in g(\mathscr{E})}
     {\Gamma \vdash \tntout{m}.E : g}
     {}
  }
     \\[3ex]
  \multicolumn{4}{c}{
     \Rulea{Open}
     {\Gamma \vdash \loc{n}{E}{B_1}{\vec{\sigma}} : g : Group,
  \Gamma \vdash \loc{m}{F}{B}{\vec{\sigma}} : h : Group,
  m \in g(\mathscr{O}),
  n \in h(\mathscr{E})}
     {\Gamma \vdash \tntopen{m}.E : g}
     {}
  }
  \\[3ex]
  \multicolumn{4}{c}{
     \Rulea{ProcIn}
  {\Gamma \vdash a : Name,
  \Gamma \vdash \loc{n}{E \mid F \mid \loc{m}{\nil}{B_1}{\vec{\sigma}}}{B_2}{\vec{\rho}} : g : Group, 
  m \in g(\mathscr{E})}
     {\loc{n}{\procin{a}{m}.E \mid a.F \mid \loc{m}{\nil}{B_1}{\vec{\sigma}}}{B_2}{\vec{\rho}} : g : Group}
     {}  
  }
  \\[3ex]
  \multicolumn{4}{c}{
     \Rulea{ProcOut}
  {\Gamma \vdash a : Name,
  \Gamma \vdash \locv{n}{\loc{m}{E \mid F}{B_1}{\vec{\sigma}}}{B_2}{\vec{\rho}} : g : Group, 
  m \in g(\mathscr{L}),
  n \in g(\mathscr{E})}
     {\Gamma \vdash \locv{n}{\loc{m}{\procout{a}{m}.E \mid a.F}{B}{\vec{\sigma}}}{B_2}{\vec{\rho}} :
  g}
     {}
  }
 \end{tabular}
  \end{center}
  \shrule
\end{table}

The mobility types form the remaining focus of our type system; the type
$g$ of an environ $\locv{m}{E}{B}{\vec{\sigma}}$ is that of its
encapsulated process $E$, subject to the constraint $m \in
g(\mathscr{R})$. Similar sanity checks are performed in the other
rules. For example, in $Open$, $E$ is the process that performs the
mobility primitive, $\tntopen{m}$ (subject to the constraint $m \in
g(\mathscr{O})$).  However, the destruction of $m$ also has an effect on
its process ($F$).  As a result, $F$ must have an appropriate type, $h$,
such that $F$ can reside in the parent environ, $n$, after $m$ is
removed.

\section{Equivalence Theory}
\label{sec:equivalence-theory}

What does it mean for two expressions $E$ and $F$ to be equivalent? We
will adopt the standard Morris-style \cite{Mor68} (or \emph{may-testing}
\cite{DNH84}) approach used to characterise both equivalence of mobile
ambients \cite{GC99} and some descriptions of barbed congruence in the $\pi$-calculus
\cite{sangiorgi:book}. 

\subsection{Observability}
\label{sec:observability}

The notion of immediate observability of an action or clock needs to take
account of possible timeouts. For example, the action $a$ can occur immediately
in both $a.\nil$ and $\timeout{a.\nil}{\sigma}{b.\nil}$, while the
action $b$ can occur immediately in neither. We can capture the required
behaviour quite simply, however, by appealing to our semantics.

\begin{definition}
We say that $E$ \emph{exhibits} the action $\alpha$, and write $E
\ExhibitsA \alpha$, provided $E \Does{\alpha}$. We say that $E$
\emph{exhibits} the clock $\sigma$, and write $E \ExhibitsT \sigma$,
provided $E \Does{\sigma}$.
\end{definition}

Gordon and Cardelli \cite{GC99} define an expression $E$ to exhibit an
environ $n$ provided $n$ occurs at top-level in $E$. We adapt this
definition to include information about bouncers and clock sets, and say that
$E$ exhibits the environ (actually an environ \emph{context})
$\locv{n}{}{B}{\vec{\sigma}}$ provided this occurs at top-level. However, our
definition again needs to take account of potential time-outs. For example,
$\loc{n}{}{B}{\rho}$ is exhibited in both $\loc{n}{E}{B}{\rho}$ and
$\timeout{\loc{n}{F}{B}{\rho}}{\sigma}{\nil}$.

\begin{definition}
We say that $E$ \emph{exhibits} the environ $\locv{n}{\,}{B}{\vec{\sigma}}$,
and write $E \ExhibitsE \locv{n}{\,}{B}{\vec{\sigma}}$, provided $E$ is 
of one of the forms

\begin{enumerate}
\item
    $\locv{n}{F}{B}{\vec{\sigma}}$; or
\item
    $\timeout{E' }{\rho}{F}$ or $\stimeout{E' }{\rho}{F}$,
    where $E' \ExhibitsE \locv{n}{\,}{B}{\vec{\sigma}}$;
\end{enumerate}
\end{definition}


A symbol $x$ is \emph{eventually observable} (we shall usually say it
is \emph{revealed}) in an expression $E$ precisely when $x$ is the
first \emph{relevant} action of the appropriate class. As usual, we
write $\DoesTaus$ for the reflexive transitive closure of $\Does{\tau}$ and 
$\Weak{\gamma}$ for $\DoesTaus\Does{\gamma}\DoesTaus$.

\begin{definition}
We say that $E$ \emph{reveals} the action $\alpha$, and write $E
\RevealsA \alpha$, provided there is some $E'$ such that $E
\DoesTaus E' \ExhibitsA \alpha$.
\end{definition}

Clocks are used to delimit activities, so we should allow non-clock transitions
to proceed between clock ticks without prejudicing the subsequent tick's
right to be considered eventually observed.

\begin{definition}
We say that $E$ \emph{reveals} the clock $\sigma$, and write $E
\RevealsT \sigma$, provided there is some $E'$ and some $\vec{\kappa} \in
\left( \actions \cup \{ \tin, \tout, \topen \}\right)^*$ such that $E
\Does{\vec{\kappa}} E' \ExhibitsT \sigma$.
\end{definition}

An environ is eventually observed provided it can be brought to top
level by some sequence of reductions.

\begin{definition}

We say that $E$ \emph{reveals} the environ $\locv{n}{\,}{B}{\vec{\sigma}}$,
and write $E \RevealsE \locv{n}{\,}{B}{\vec{\sigma}}$, provided there is
some $E'$ and some $\vec{\gamma}$ such that $E \Does{\vec{\gamma}}
E' \ExhibitsE \locv{n}{\,}{B}{\vec{\sigma}}$.

\end{definition}


\subsection{Contextual Congruence}
\label{sec:contextual-congruence}

Before we can define contextual congruence, we need to decide what it is for 
two expressions to reveal the \emph{same} environ. Our definition is
recursive, since the equivalence of $\locv{m}{}{E}{\vec{\sigma}}$ and
$\locv{n}{}{F}{\vec{\rho}}$ relies on the equivalence of $E$ and
$F$.

As usual, a \emph{context} $C$ is an expression with one or more
\emph{holes}. We write $[\,]$ for a hole, and $C[E]$ for the expression
obtained by filling $C$'s holes with copies of $E$ (this may result
in free names and variables in $E$ becoming bound).

\begin{definition}

We say that $E$ and $F$ are (contextually) \emph{congruent}, and write
$E \Eq F$, if for all contexts $C$, expressions $E$ and
$F$, $\alpha \in \actions$, $\sigma \in \timers$, and environs
$\locv{n}{\,}{B}{\vec{\sigma}}$,

\begin{enumerate}
\item
     $C[E] \RevealsA \alpha \Longleftrightarrow C[F] \RevealsA \alpha$;
     we say the expressions are \emph{action equivalent}, written $E \EqA
     F$; 
\item
     $C[E] \RevealsT \sigma \Longleftrightarrow C[F] \RevealsT \sigma$; we
     say the expressions are \emph{timer equivalent}, written   $E \EqT
     F$; 
\item
     they reveal the same environs (up to equivalence of bouncers) in every 
     context:
     \begin{enumerate}
     \item
        If $C[E] \RevealsE \locv{n}{\,}{E'}{\vec{\sigma}}$ then
        $C[F] \RevealsE \locv{n}{\,}{F'}{\vec{\sigma}}$
        for some $F' \Eq E'$;
     \item
        If $C[F] \RevealsE \locv{n}{\,}{F'}{\vec{\sigma}}$ then
        $C[E] \RevealsE \locv{n}{\,}{E'}{\vec{\sigma}}$
        for some $E' \Eq F'$.
     \end{enumerate}
     We say the expressions are \emph{environ equivalent}, written $E \EqE 
     F$.
\end{enumerate}

\end{definition}


\begin{proposition}
\label{prop:context-substitution} 
Suppose $E \Eq F$. Given any context $C$, we have $C[E]
\Eq C[F]$.
\end{proposition}
\begin{proof}
Given any context $C'$, let $C'[C]$ be the result of filling the
holes in $C'$ with copies of $C$. Then $C'[C]$ is itself a context,
whence $C'[C[E]]$ and $C'[C[F]]$ reveal the same actions,
clocks and environs. Since $C'$ was arbitrary, we have $C[E] \Eq
C[F]$, as claimed.
\qed \end{proof}

\begin{theorem}
The relation $\Eq$ is a congruence on TNT expressions. \qed
\end{theorem}



Proving that two expressions are not congruent is generally easy. For
example, $a.\nil \NotEq b.\nil$ because $a.\nil$ reveals $a$
but $b.\nil$ doesn't. Proving congruence is
more difficult. We illustrate the technique we use by proving the simple
congruence $\left(a. E \res{a}\right) \Eq \nil$, which is useful
for tidying up expression reductions. Our proof technique relies on the
nature of reductions in contextual expressions.

Suppose the context $C$ contains $n$ holes; we will write
$C[\,]_1\dots[\,]_n$. Then $C[E]$ means $C[E]_1\dots[E]_n$. If
$E \Does{x} E'$, then (depending on the nature of $C$), it is possible
that $C[E] \Does{x} C[E]_1\dots[E']_j\dots[E]_n$ for some $j$.
We say that such a transition is \emph{local} to $E$ in $C$. On the other
hand, there are some transitions that $C[E]$ can perform, regardless of
$E$. We call these transitions \emph{global} in $C$. For example, the
transition \[ \out{a}.[\,] \mid a . b . [\,] \quad\Does{\tau}\quad [\,]
\mid b . [\,] \] is global. All other transitions in $C[E]$ are
\emph{distributed}.

\clearpage
Distributed transitions are those that involve reduction of subcontexts of the
form $C'|[\,]$, $C' + [\,]$ and $\locv{n}{\,}{B}{\vec{\sigma}}$. For example,

\begin{itemize}
\item
    $\nil + a.\nil \Does{\sigma}$ but $\nil + \Delta_\sigma
     \not\Does{\sigma}$, so clock transitions are distributed in the
     context $\nil + [\,]$.
\item
    $a.\nil \mid \out{a}.\nil \Does{\tau}$ but $a.\nil \mid
     \nil \not\Does{\tau}$, so $\Does{\tau}$ is distributed in the
     context $a.\nil \mid [\,]$.
\item
    $\locv{m}{ \locv{n}{\tntout{m}.\nil}{B}{\vec{\sigma}}}%
     {\bout.\Omega}{\vec{\rho}} ~\Does{\tout}$ but
    $\locv{m}{ \nil }{\bout.\Omega}{\vec{\rho}} ~\not\Does{\tout}$,
     so $\Does{\tout}$ is distributed in the context $\locv{m}{\,}%
     {\bout.\Omega}{\vec{\rho}}$.
\end{itemize}
The following results are immediate.

\begin{proposition}
Suppose $E \not\Does{x}$ where $x$ is either $a$ or $\sigma$. If
$C[E] \Does{x}$ then the $\Does{x}$ transition is global.
The only distributed transitions are $\Does{\sigma}$, $\Does{\tau}$,
$\Does{\tin}$, $\Does{\tout}$ and $\Does{\topen}$.
\qed \end{proposition}

We can now prove the congruence claimed above. To see that $\left(a. E
\res{a}\right) \Eq \nil$, we observe that $\left(a. E \res{a}\right)$
cannot reveal any actions. Consequently, any visible action in $C[a. E
\res{a}]$ must be global, and hence revealed by $C[\nil]$. Moreover, the lack of
visible actions means that $\Does{\tau}$ cannot be generated by interaction
between $a. E \res{a}$ and a neighbouring subexpression. Therefore,
$\left(a. E \res{a}\right) \EqA \nil$. Since neither expression can
reveal top-level environs or mobility transitions, they cannot contribute to
distributed mobility transitions in any context $C$, whence $\left(a. E
\res{a}\right) \EqE \nil$. Finally, we note that both expressions reveal all
clocks $\sigma$, so that $\left(a. E \res{a}\right) \EqT \nil$, and we
are done.


\subsection{Located Temporal Observation Congruence}
\label{sec:ltoc}

Following an idea in \cite{case}, we now use $\Eq$ to define a
subcongruence $\LTOC$ which adds bisimulation properties to the
contextual equivalence described above.

\begin{definition}

A symmetric relation $R\mathrel{\subseteq}\mathop{\EqE}$ is a
\emph{located temporal observation equivalence (l.t.o.e.)} if for every
context $C$, and every $(E,F) \in R$, $\kappa \in \actions \cup
\{ \tntin, \tntout, \tntopen \}$, $\vec{\kappa} \in \left(\actions \cup
\{ \tntin, \tntout, \tntopen \}\right)^*$ and $\sigma \in \timers$,

\begin{enumerate}
\item
    $C[E] \Weak{\kappa} E' \mbox{ implies }
       \exists F' ~.~ C[F] \Weak{\kappa} F' \mbox{ and } E' \Eq F' \mbox{ and } (E', F') \in R$ 
\item
    $C[E] \Does{\vec{\kappa}}\Does{\sigma} E' \mbox{ implies }
       \exists \vec{\kappa}', F' ~.~ 
       C[F] \Does{\vec{\kappa}'}\Does{\sigma} F' \mbox{ and } (E', F') \in R$
\end{enumerate}
We write $E \LTOC F$ if $(E,F) \in R$ for some l.t.o.e. $R$.
\end{definition}

In view of the following result, which follows immediately from the
definitions, we call the relation, $\LTOC$, \emph{located temporal
observation congruence} (l.t.o.c.).

\begin{lemma}
The equivalence $\LTOC$ is a subcongruence of $\Eq$. \qed
\end{lemma}

We do not know at present whether the two congruences are in fact
identical. To give a flavour of the sorts of elementary proofs that can
be generated using l.o.t.c., we conclude this section by proving a
useful cancellation lemma.

\begin{definition}
Given any expression $E$ and any visible action $a \in
\actions\setminus\tau$, the process $E\After{a}$, pronounced
\emph{$E$ after $a$}, is defined by
\[
    E\After{a} \eqdef \sum \{ E' \mid E \Weak{a} E' \}
\]
\end{definition}

Notice that $\Weak{a}$ need not be image-finite -- consider, for
example, the process $\mu X .(\tau. X + a.\nil)$. In such cases
the operator $\After{a}$ is not well-defined in the stated formulation.

\begin{theorem}[Cancellation Lemma]
\label{thm:cancellation}

Suppose given the expressions $E$, $F$ and any visible action
$a \in \actions\setminus\tau$ for which $F$ has only finitely many
$\Weak{a}$ derivatives. Then
\[
    a. E ~\LTOC~ F 
    \quad\Longrightarrow\quad 
    E ~\LTOC~ F\After{a}
\]
\end{theorem}
\begin{proof}

Suppose $R$ is some l.t.o.e. with $(a. E,F) \in R$. We know
that $a. E \Does{a} E$ must be matched by a move $F
\Weak{a} F'$ where $(F', E) \in R$.

Suppose $E \Weak{\kappa} E'$. Then there exists some $F''$
such that $F' \Weak{\kappa} F''$ and $(F'',E') \in
R$. However, $F'$ is one of the summands of $F\After{a}$, so
the latter can also perform the transition $F\After{a}
\Weak{\kappa} F''$ with $(F'',E') \in R$, as required.

Conversely, suppose $F\After{a} \Weak{\kappa} F''$. Since
$F\After{a}$ is a sum, we know that one of its summands,
$F'''$ (say), can perform the same transition sequence: $F'''
\Weak{\kappa} F''$. By definition, we have $F \Weak{a}
F'''$, which must be matched by some derivation $a. E
\Weak{a} E'$ with $(F''', E') \in R$. Thus $E'
\Weak{\kappa} E''$ with $(E'',F'') \in R$. However, we know
that the only non-clock transition $a.E$ can perform initially is
$a$. Consequently, the derivation $a.E \Weak{a} E'$ can be
factorised as $a.E \Does{a} E \DoesTaus E'$. Putting the
pieces together gives
\[
    a. E \Does{a} E \DoesTaus E' \Weak{\kappa} E''
\]
or in other words, $E\Weak{\kappa} E''$ where
$(E'',F'') \in R$, as required.

The proof for clock transitions is similar.
\qed \end{proof}

\section{Conclusions and Future Work}
\label{futurework}

We have presented a novel combination of process synchronisation and
timed mobility, and introduced the concept of synchronisation-based
objective process mobility and specific security processes; these are
believed to be new to the field of process algebra.  The resulting
process calculus is designed to provide a sufficient framework to tackle
the concepts mentioned in the introduction.

We have also introduced two congruence relations on TNT expressions, and
used them to develop an equivalence theory. Both congruences
respect the underlying motivation for our work; in particular, the
equivalence of clock behaviours captures the idea that workflow
progresses by distinct stages. Our second congruence, located temporal
observation congruence, combines aspects of simulation and contextual
equivalence, enabling us to prove results using techniques from either
approach.

With regard to future work, we have begun development of a tool,
DynamiTE (\emph{Dynamic Theory Execution}), which will allow both
simulation of TNT processes and a mapping of these onto
Java\footnote{While a functional programming language like Haskell may
provide a simpler theoretical framework, we consider Java to be
industrially more relevant, and to provide greater opportunity for less
theoretically inclined developers.} and its underlying concurrency
model.  In the long term, we are considering further extensions to the
calculus, including the generalisation of bouncers to a general property
attachment mechanism for environs.  This will allow us, for example, to
associate environs with stochastic measures, to give a stochastic
variant of the calculus.  In the type system, an inferencing algorithm
would be beneficial to avoid the current reliance on a pre-populated
type environment.

\subsection*{Acknowledgements}

We would like to thank Simon Foster, Gerald L{\"u}ttgen, Barry Norton
and Georg Struth for their helpful comments and suggestions.  This work
is partially supported by the Engineering and Physical Sciences Research
Council ({EPSRC}).

\bibliographystyle{splncs}
\bibliography{literature}

\end{document}